T:Type, R:(TT), L:(T List), x, y, z:T.
rel-path-between(T;R;x;y;[z / L])
 (x = z
 & ((null(L))  (y = z))
 & (((null(L)))  ((x R hd(L)) & rel-path-between(T;R;hd(L);y;L)))) 

latex

Definitions

#$n, t  T, s = t, x:AB(x), x:A. B(x), ||as||, n+m, Type, type List, P  Q, A, , A  B, i  j , b, True, False, a < b, Void, rel-path(R;L), [car / cdr], last(L), hd(l), [], f(a), x f y, i <z j, i z j, l[i], , x:A  B(x), P & Q, <a, b>, , null(as), A c B, -n, n - m, i  j < k, {x:A| B(x)} , {i..j}, Top, S  T, x:A.B(x), P  Q, A List, (x  l), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , P  Q, rel-path-between(T;R;x;y;L), , tl(l), , T, s ~ t, {T}, SQType(T), left + right, P  Q, Dec(P), Atom, x,y:A//B(x;y), x:A. B(x), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, |r|, xL. P(x), (xL.P(x)), Unit,

Lemmas

decidable int equal, guard wf, last-cons, select cons tl, true wf, squash wf, nat wf, le wf, subtype rel wf, iff wf, rev implies wf, length cons, null wf3, member wf, top wf, last wf, not wf, assert wf, false wf, int seg wf, select wf, hd wf, rel-path wf, non neg length, length wf1